FDL - Nuprl Lemma : union-codes_wf

Nuprl Lemma : union-codes_wf

es:ES, C, T:Type, S1, S2:(C

C

E

), codes1:(j,i:C

e:{x:E| S1(j,i,x)}

state@loc(e)

T),

codes2:(j,i:C

e:{x:E| S2(j,i,x)}

state@loc(e)

T), dec_S1:(j,i:C

e:E

Dec(S1(j,i,e))).
[S1? codes1 : codes2]

j,i:C

e:{x:E| (S1(j,i,x))

(S2(j,i,x))}

state@loc(e)

T

Definitions ES, , Type, x:A. B(x), Dec(P), P Q, x:AB(x), state@i, {x:A| B(x)} , left + right, f(a), E, t T, [S? codes1 : codes2], x.A(x), loc(e), if p:P then A(p) else B fi , s = t, P Q, A, False

Lemmas es-loc wf, es-state wf, es-E wf